\begin{tabbing}
$\forall$\=$A$:Type, $l$:IdLnk, ${\it tg}$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)).
\-\\[0ex]($\forall$$k$:Knd. ($\uparrow$$k$ $\in$ dom(${\it conds}$)) $\Rightarrow$ ($\uparrow$hasloc($k$;source($l$))))
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal($A$)
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ fpf{-}domain(${\it conds}$)) $\Rightarrow$ ((${\it conds}$($k$).1) \& ($\neg$($k$ = rcv($l$,${\it tg}$)))))
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.triggers{-}glued{-}p(${\it es}$; $A$; $l$; ${\it tg}$; ${\it ds}$; ${\it conds}$)
\end{tabbing}